\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$,$B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$f$:(($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$).
\-\\[0ex]ecl{-}trans{-}normal($A$)
\\[0ex]$\Rightarrow$ ecl{-}trans{-}normal($B$)
\\[0ex]$\Rightarrow$ ($\forall$$m$:$\mathbb{N}$. $\neg$($\uparrow$($f$(($\lambda$$n$.ff),$\lambda$$n$.ff,$m$))))
\\[0ex]$\Rightarrow$ ecl{-}trans{-}normal(combine{-}ecl{-}tuples($A$; $B$; $f$; $g$))
\end{tabbing}